es:ES, A:Type, k:Knd, l:IdLnk, tg:Id, B:Type, ds:x:Id fp Type,
f:(z:x:Id. vartype(source(l);x) r ds(x)?Top.{e:E| loc(e) = source(l)  Id & (valtype(e) r A)} 
f:((?B)).
state dsk:A sends [tg, e.f(e):B] on l   

latex

Definitions

t  T, x:A. B(x), E, s = t, x:A  B(x), P & Q, A c B, {T}, P  Q, sender(e), let x,y = A in B(x;y), t.1, b, Type, x:AB(x), kind(e), Knd, rcv(l,tg), e@i. P(e), if b then t else f fi , ES, left + right, IdLnk, Atom$n, Id, a:A fp B(a), x:A.B(x), case b of inl(x) => s(x) | inr(y) => t(y), valtype(e), source(l), loc(e), {x:A| B(x)} , <a, b>, f(a), Unit, x(s), outl(x), val(e), isl(x), , , x:A. B(x), x. t(x), Top, IdDeq, x.A(x), f(x)?z, vartype(i;x), state dsk:A sends [tg, e.f(e):B] on l

Lemmas

fpf wf, IdLnk wf, event system wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, alle-at wf, assert wf, isl wf, es-val wf, outl wf, unit wf, Id wf, es-loc wf, lsrc wf, es-valtype wf, rcv wf, Knd wf, es-kind wf, es-sender wf, es-kind-rcv, es-E wf